\begin{tabbing}
$\forall$\=${\it es}$:ES, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $n$:$\mathbb{N}$, $a$:ecl(${\it ds}$;${\it da}$),\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?!Void()).
\-\\[0ex]es{-}decls(${\it es}$;source($l$);${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=(\=with decls \=${\it ds}$ \+\+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if kind($e$) = $k$ $\wedge_{b}$ action[[$a$ $n$]][es{-}init(${\it es}$;$e$);$e$]\+
\\[0ex]then [$<$${\it tg}$, $f$((state when $e$),val($e$))$>$]
\\[0ex]else []
\\[0ex]fi  
\-\\[0ex]and only these for tags in [${\it tg}$]
\-\\[0ex]$\Leftarrow\!\Rightarrow$ \=es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;${\it da}$(rcv($l$,${\it tg}$))?Top;${\it ds}$;$e$.kind($e$) = $k$\+
\\[0ex]\& ecl{-}es{-}act(${\it es}$;$n$;$a$)(es{-}init(${\it es}$;$e$),$e$);$e$.$f$((state when $e$),val($e$))))
\-\-
\end{tabbing}